#include "cdcl_dependence_graph.h"
#include<stdlib.h>
#include<stdio.h>
#include<malloc.h>
extern int max_var_id;

void free_literal_set(literal_set* ls){
    //printf("try free literals %p\n", ls->literals);
    free(ls->literals);
    ls->literals = NULL;
    //printf("try free is_in_set %p\n", ls->is_in_set);
    free(ls->is_in_set);
    ls->is_in_set = NULL;
    //printf("try free self %p\n", ls);
    
    free(ls);
    // ls = NULL;
    //printf("ok\n");
}
void literal_free(DGliteral* l, int decision){
    assert(l->parents != NULL);
    assert(l->children != NULL);
    if(decision){
        //printf("imply %p\n", ((DGDecisionLiteral*)l)->implies);
        free_literal_set(((DGDecisionLiteral*)l)->implies);
    }
    //printf("free parent %p,child %p, self %p\n", l->parents, l->children, l);
    free_literal_set(l->parents);
    l->parents = NULL;
    //free(l->parents);
    //printf("freed var %d 's parent\n", l->varname);
    free_literal_set(l->children);
    l->children = NULL;
    //free(l->children);
    //printf("freed var %d 's child\n", l->varname);
    free(l);
    //printf("self\n");
}

static int literal_hash(__uint16_t name, __uint16_t sign){
    int ret = name<<1;
    return sign ? ret : ret + 1;
}

static int literal_neghash(__uint16_t name, __uint16_t sign){
    int ret = name<<1;
    return sign ? ret + 1 : ret;
}



literal_set* new_literal_set(){
    literal_set* ls = malloc(sizeof(literal_set));
    //printf("malloc ls is %p, size is %d\n",ls, 2* sizeof(int) * max_var_id);
    ls->is_in_set = (int*)malloc(2* sizeof(int) * max_var_id);
    //printf("malloc is in set is %p\n",ls->is_in_set);

    ls->literals = malloc(2 * sizeof(DGDecisionLiteral*) * max_var_id);
    //printf("malloc literals is %p\n",ls->literals);

    for(int i = 0; i < 2 * max_var_id; i++){
        ls->is_in_set[i] = 0;
        ls->literals[i] = NULL;
    }

    return ls;
}

DGliteral* set_find(literal_set* ls, DGliteral* l){
    int hash = literal_hash(l->varname, l->varsign);
    if (ls->is_in_set[hash]) return ls->literals[hash];
    else return NULL;
}

void set_add_literal(literal_set* ls, DGliteral* l){
    assert(ls != NULL);
    int hash = l->varname << 1;
    hash = l->varsign ? hash : hash+1;

    //printf("set_add_literal %p = %p + %d * %d \n", &ls->is_in_set[hash], ls, sizeof(int),hash);
    if(ls->is_in_set[hash] > 0){
        //printf("ADD SAME LITERAL AGAIN, name %d\n", l->varname);
        return;
        //assert(0);
    }
    else{
        ls->is_in_set[hash] = 1;
        ls->literals[hash] = l;
    }
}

int set_num(literal_set* ls){
    int num = 0;
    for(int i = 0; i < max_var_id* 2; i++){
        if (ls->is_in_set[i]) num++;
    }
    return num;
}

DGliteral* set_get_first(literal_set* ls){
    for(int i = 0; i < max_var_id* 2; i++){
        if (ls->is_in_set[i]) return ls->literals[i];
    }
    return NULL;
}

void set_erase(literal_set* ls, DGliteral* l){
    int hash = literal_hash(l->varname, l->varsign);
    ls->is_in_set[hash] = 0;
    assert(ls->literals[hash]->parents != NULL);
    ls->literals[hash] = NULL;
    // printf("erase %d success\n",l->varname);
}

DGliteral* new_literal(__uint16_t name, __uint16_t sign){
    DGliteral* ret = malloc(sizeof(DGDecisionLiteral));
    ret->varname = name;
    ret->varsign = sign;
    ret->type = UNKNOWN;
    //init sets
    ret->children = new_literal_set();
    ret->parents = new_literal_set();  

  
    //printf("init literal parent %p , child %p, self %p\n",  ret->parents, ret->children, ret);

    for(int i = 0; i < 2 * max_var_id; i++){
        assert(ret->parents->is_in_set[i] == 0);
        assert(ret->parents->literals[i] == NULL);
        assert(ret->children->literals[i] == NULL);
        assert(ret->children->is_in_set[i] == 0);
    }
    return ret;
}

DGDecisionLiteral* new_decision_literal(__uint16_t name, __uint16_t sign){
    DGliteral* ret = new_literal(name, sign);
    ret->type = DECISION;    
    assert(&(((DGDecisionLiteral*)ret)->literal) == ret);
    ((DGDecisionLiteral*)ret)->implies = new_literal_set();
    return (DGDecisionLiteral*)ret;
}
//extern DGliteral* parentdecision;

DGStandardLiteral* new_standard_literal(DGliteral* parentdecision, __uint16_t name, __uint16_t sign){
    DGliteral* ret = new_literal(name, sign);
    
    ret->type = STANDARD;
    ret->implied_by = parentdecision;
    if(parentdecision != NULL){
        //printf("parentdecision (%d ,%d)add imply (var:%d,sign:%d)\n", parentdecision->varname, parentdecision->varsign, ret->varname, ret->varsign);
        set_add_literal(((DGDecisionLiteral*)parentdecision)->implies, ret);
    }else{
        printf("no parentdecision\n");
    }
    return (DGStandardLiteral*)ret;
}

void literal_add_child(DGliteral* l, DGliteral* child){
    //printf("var%d sign%d add child var%d sign%d \n",
    //l->varname, l->varname, child->varname, child->varsign);
    set_add_literal(l->children, child);   
}

void Decision_add_imply(DGDecisionLiteral* l, DGliteral* imp){
    //printf("var%d sign%d add imply var%d sign%d \n",  
    //l->literal.varname, l->literal.varsign, imp->varname, imp->varsign);  
    set_add_literal(l->implies, imp);
}

static DGliteral* _graph_find(DGraph* g, int hash){
    if (g->lookup_map->is_in_set[hash] > 0){
        return g->lookup_map->literals[hash];
    }
    //print_graph(g);
    return NULL;
}

DGliteral* graph_find(DGraph* g, const variable* v){
    int hash = literal_hash(v->name, v->sign);
    //printf("graph_find var:%d, sign%d, hash%d\n", v->name, v->sign, hash);
    return _graph_find(g, hash);
}

DGliteral* graph_find_negation(DGraph* g, const variable* v){
    assert(v != NULL);
    int hash = literal_neghash(v->name, v->sign);
    //show_graph_nodes(g);
    //printf("graph_find_negation var:%d, sign%d, hash%d\n", v->name, v->sign, hash);
    return _graph_find(g, hash);
}


/**
 * Adds a literal to the dependency graph
 */
void graph_add_node(DGraph* g, DGliteral*l){
    DGliteral* same = _graph_find(g, literal_hash(l->varname, l->varsign));
    DGliteral* neg  = _graph_find(g, literal_neghash(l->varname, l->varsign));
    if(neg != NULL){
        g->has_conflict = true;
        g->conflict = l->varname;
        //printf("conflict happened");
        //printf("conflict happened on var %d\n", l->varname);
    }
    if(same != NULL){
        printf("attempting to add the same literal twice: %d", l->varname);
        assert(0);
    }    
    set_add_literal(g->lookup_map, l);
    //printf("success add to graph: var %d, sign %d\n", l->varname, l->varsign);
}

void remove_node(DGraph* graph, DGliteral* l){
    if (l->type ==STANDARD){
        printf("you should not remove a standard node\n");
        assert(0);
    }
    else if (l->type == DECISION){
        DGDecisionLiteral* dl = (DGDecisionLiteral*)l;
        for(int i = 0; i < 2 * max_var_id; i++){
            if (dl->implies->is_in_set[i]){
                DGliteral* imp = dl->implies->literals[i];
                for(int j = 0; j < 2 * max_var_id; j++){
                    if(imp->children->is_in_set[j]){
                        DGliteral* c = imp->children->literals[j];
                        set_erase(c->parents, imp);
                    }
                }
                set_erase(graph->lookup_map, imp);
                set_add_literal(graph->free, imp);
                //printf("###add to free %p var: %d, sign %d\n", imp, imp->varname, imp->varsign);
                assert(imp->parents!= NULL);
                //free imp
            }
        }
        //free l
        set_erase(graph->lookup_map, l);
        set_add_literal(graph->free, l);
        //printf("###add to free %p var %d sign %d\n", l, l->varname, l->varsign);
        assert(l->parents != NULL);
    }
}

DGraph* new_graph(){
    DGraph* g = malloc(sizeof(DGraph));
    g->lookup_map = new_literal_set();
    g->free = new_literal_set();
    g->conflict = -1;
    g->has_conflict = false;
    return g;
}

void show_graph_nodes(DGraph* g){
    printf("{\n");
    for(int i = 0; i < 2 * max_var_id; i++){ 
        if (g->lookup_map->is_in_set[i]){
            DGliteral* l = g->lookup_map->literals[i];
            if (l->type == STANDARD){
                printf("  [STANDARD] name: %d, sign; %d\n", l->varname, l->varsign);
            }else{
                printf("  [DECISION] name: %d, sign; %d\n", l->varname, l->varsign);
            }
        }    
    }
    printf("}\n");
}

void _print_graph_r(DGliteral* l){
    if(l == NULL){
        assert(0);
    }
    if(l->type == STANDARD){
        printf("\n[STANDARD] name: %d, sign; %d\n", l->varname, l->varsign);
    }else{
        printf("\n[DECISION] name: %d, sign; %d\n", l->varname, l->varsign);
    }

    if (l->type == STANDARD){
        assert(l->children != NULL);
        printf("childs => {\n");
        for(int i = 0; i < 2 * max_var_id; i++){
            if(l->children->is_in_set[i]){
                DGliteral* c = l->children->literals[i];
                printf("[name:%d,sign:%d], ", c->varname, c->varsign);
            }
        }
        printf("}\n");    
    }else{
        printf("implies => {\n");
        DGDecisionLiteral* dl = (DGDecisionLiteral*)l;
        assert(dl->implies != NULL);
        
        for(int i = 0; i < 2 * max_var_id; i++){
            if(dl->implies->is_in_set[i]){
                DGliteral* c = dl->implies->literals[i];
                assert(c != NULL);
                printf("[name:%d,sign:%d], ", c->varname, c->varsign);
            }
        }
        printf("}\n"); 
        printf("childs =>{\n");
        for(int i = 0; i < 2 * max_var_id; i++){
            if(dl->literal.children->is_in_set[i]){
                DGliteral* c = dl->literal.children->literals[i];
                if(c->type == STANDARD){
                    printf("STD[name:%d,sign:%d],\n ", c->varname, c->varsign);
                }
                else{
                    printf("DEC[name:%d,sign:%d],\n ", c->varname, c->varsign);
                }
            }
        } 
        printf("}\n");
        for(int i = 0; i < 2 * max_var_id; i++){
            if(dl->literal.children->is_in_set[i]){
                _print_graph_r(dl->literal.children->literals[i]);
            }
        }
    }   
}
void print_graph(DGraph*g){
    assert(g->lookup_map != NULL);
    DGliteral* l = set_get_first(g->lookup_map);
    if (l == NULL){
        printf("empty graph\n");
        return;
    }
    DGliteral* p = set_get_first(l->parents);

    while (p != NULL){
        l = p;
        p = set_get_first(p->parents);
    } 
    //now l is the root;
    _print_graph_r(l);
}